#!/bin/bash
umask u=rwx,g=rx,o=rx

make
strip cbmc

VERSION=`./cbmc --version | cut -d " " -f 1`
VERSION_FILE=`echo $VERSION | sed "y/./-/"`
BITS=`getconf LONG_BIT`
# UNAME_M=`uname -m`
DEB_ARCH=`dpkg --print-architecture`

echo $VERSION_FILE

(cd ../goto-cc; make; strip goto-cc)
(cd ../goto-instrument; make; strip goto-instrument)

mkdir /tmp/cbmc-dist
cp ../cbmc/cbmc ../goto-cc/goto-cc \
  ../goto-instrument/goto-instrument /tmp/cbmc-dist/
cp ../../LICENSE /tmp/cbmc-dist/
cp ../../doc/man/cbmc.1 /tmp/cbmc-dist/
cd /tmp/cbmc-dist
tar cfz cbmc-${VERSION_FILE}-linux-${BITS}.tgz cbmc \
  goto-cc goto-instrument LICENSE

mkdir debian
mkdir debian/DEBIAN
mkdir debian/usr
mkdir debian/usr/bin
mkdir debian/usr/share
mkdir debian/usr/share/man
mkdir debian/usr/share/man/man1
cp cbmc goto-cc goto-instrument \
  debian/usr/bin/
cp cbmc.1 debian/usr/share/man/man1

cat > debian/DEBIAN/control << EOM
Package: cbmc
Version: $VERSION
Section: devel
Priority: optional
Architecture: ${DEB_ARCH}
Essential: no
Depends: gcc
License: BSD-4-clause
Recommends: mozilla | netscape  
Suggests: docbook 
Installed-Size: 4971
Upstream-Contact: Daniel Kroening [kroening@cs.ox.ac.uk]
Provides: cbmc
Description: CBMC is a Bounded Model Checker for C and C++ programs.
 .
 CBMC generates traces that demonstrate how an assertion can be violated,
 or proves that the assertion cannot be violated within a given number
 of loop iterations.
EOM

echo Building cbmc_${VERSION}_${DEB_ARCH}.deb 
dpkg -b debian cbmc_${VERSION}_${DEB_ARCH}.deb 

echo Copying.
scp cbmc-${VERSION_FILE}-linux-${BITS}.tgz \
    cbmc_${VERSION}_${DEB_ARCH}.deb \
  kroening@dkr-srv.cs.ox.ac.uk:/srv/www/cprover.org/cbmc/download/

cd /tmp
rm -R /tmp/cbmc-dist
